\documentclass[a4paper,10pt]{article}
\usepackage[top=2.5cm,bottom=2.5cm, left=2.5cm, right=2.5cm]{geometry}

\usepackage[utf8]{inputenc}

\usepackage{hyperref}
\usepackage{amsmath}
\usepackage{amstext}
\usepackage{amssymb}
\usepackage{amsfonts}
\usepackage{bbm}
\usepackage{latexsym}
\usepackage{pifont}
\usepackage{stmaryrd}
\usepackage{wasysym}
\usepackage{latexsym}
\usepackage{paralist}
\usepackage{enumerate}
\usepackage{booktabs}
\usepackage{alltt}
\usepackage{graphicx}
\usepackage{verbatim}
\usepackage{color}
% \usepackage[T1]{fontenc}
%\usepackage{txfonts} % super tt called "txtt"

\input{custom} % from curr-dhsr-subdir

\newcommand{\fnurl}[1]{\footnote{\url{#1}}}
\newcommand{\entry}[1]{\paragraph*{#1}}
\renewcommand{\comment}[1]{[#1]}

\newcommand{\redsp}{\vspace{-1.5ex}} % hack for nested li environments
%

\parindent=0cm

% \setcounter{tocdepth}{3}
% \setcounter{secnumdepth}{3}

\def\mi#1{\mathit{#1\/}}
\def\hnum#1{\hbox{$#1$\/}}
\def\lar{\leftarrow}
\def\no{\ii{not}}
\def\ii#1{\hbox{\sl #1\/}}
\def\bb#1{\hbox{\bf #1\/}}
\def\ba{\begin{array}}
\def\ea{\end{array}}
\def\be{\begin{enumerate}}
\def\ee{\end{enumerate}}
\def\bi{\begin{itemize}}
\def\ei{\end{itemize}}
\def\beq{\begin{equation}}
\def\eeq#1{\label{#1}\end{equation}}
\def\beeq{\begin{equation*}}
\def\eeeq{\end{equation*}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\newcommand{\LFP}{\textsc{LFP}}
\newcommand{\IFP}{\textsc{IFP}}
\newcommand{\PFP}{\textsc{PFP}}
\newcommand{\DATALOG}{\textsc{DATALOG}}
\newcommand{\Ptime}{\textsc{Ptime}}

\begin{document}

\section{Fixed Point Logics and Complexity Classes}

\bi
\item most logics we have seen cannot express many tractable graph properties: graph connectivity, reachability..
\item the limited expressiveness of FO and counting logics is due to the fact that they lack mechanisms for expressing fixed point computations.
\item example: the transitive closure query....
\[ R^\infty=\bigcup_{i=0}^\infty R^i \]
\item we study logics extended with operators for computing fixed points of various operators. 

Outline:
\bi
\item basics of fixed point theory
\item various extensions of FO with fixed point operators
\item show how to extend FO with an operator for computing just the transitive closure
\ei
\ei

\subsection{Fixed Points of Operators on Sets}

The theory of fixed point operators is presented for complete lattices: partially ordered sets $\langle U, \prec \rangle$ where every – finite or infinite – subset
of $U$ has a greatest lower bound and a least upper bound in the ordering $\prec$
\bi
\item we deal only with finite sets
\ei

Given a set $U$, let $p(U)$ be its powerset. An \ii{operator} on $U$ is a mapping $F: p(U) \rightarrow p(U)$. 
\bi
\item An operator $F$ is \ii{monotone} if $X \subseteq Y$ implies $F(X) \subseteq F(Y)$
\item and \ii{inflationary} if $X \subseteq F(X)$ 
\ei
for all $X \in p(U)$.

Given an operator $F: p(U) \rightarrow p(U)$, a set $X \subseteq U$ is a \ii{fixed point} of $F$ if $F(X)=X$. A set $X \subseteq U$ is a \ii{least fixed point} of $F$ if it is a fixed point, and for every other fixed point $Y$ of $F$ we have $X \subseteq Y$. denoted by $\bb{lfp}(F)$.

Consider the sequence:
\beq
X^0 = \emptyset, X^{i+1} = F(X^i)
\eeq{eqn:seq}

$F$ is \ii{inductive} if the sequence \eqref{eqn:seq} is increasing: $X^i \subseteq X^{i+1}$ for all $i$.
\bi
\item Every monotone operator $F$ is inductive.
\ei

If $F$ is inductive, we define
\beq
X^\infty=\bigcup_{i=0}^\infty X^i
\eeq{eqn:fixed}

Since $U$ is finite, there is a number $n$ such that $X^\infty=X^n$.
\\

Example: Let $R$ be a binary relation on a finite set $A$, and let $F: p(A^2)\rightarrow p(A^2)$ be the operator defined by $F(X)=R \cup (R \circ X)$
 
$R \circ X=\{ (a,b) \mid (a,c) \in R, (c,b) \in X, \hbox{ for some } c \in A\}$

\bi
\item this operator is monotone: if $X \subseteq Y$, then $R \circ X\subseteq R\circ Y$.
\item we will define the sequence $X^i,i\geq 0$.
\beeq \ba l
X^0=\emptyset\\
X^1=R \circ \emptyset=R\\
X^2=R \cup (R \circ R)=R \cup R^2\\
\cdots\\
X^i=R \cup \dots \cup R^i
\ea \eeeq
\item the set of pairs connected by paths of length at most $i$
\item the sequence reaches a fixed point $X^\infty$, which is the transitive closure of $R$.
\ei

\paragraph{Theorem (Tarski-Knaster)} Every monotone operator $F: p(U) \rightarrow p(U)$ has a least fixed point $\bb{lfp}(F)$, which can be defined as
$$\bb{lfp}(F) = \bigcap\{Y \mid Y=F(Y)\}.$$
Furthermore, $\bb{lfp}(F)= X^\infty = \bigcup_i X^i$, for the sequence $X^i$ defined by \eqref{eqn:seq}.

Proof:
\bi
\item Let $W=\{Y\mid F(Y) \subseteq Y\}$. We first show that $S=\bigcap W$ is a fixed point of $F$.
%  \bi
  % \item ``$W \neq \emptyset$, since~$U \in W$''. $U$ is the entire
  % set. thus, it cannot become larger. $\Rightarrow$ $F(U) \subseteq U$.
  % conseq. $U \in W$.
  % \item since $S$ is intersection of all $Y$, clearly $S \subseteq Y$.
  % \item by mon. $F(S) \subseteq F(Y)$, and since $Y \in W$, $F(Y) \subseteq Y$
  % \item $F(S) \subseteq ?? \subseteq \bigcap W \subseteq Y$.
%  \ei
\item Let $W'=\{Y \mid F(Y)=Y\}$ and $S'=\bigcap W'$.
\item $\bb{lfp}(F)=\bigcap\{Y\mid Y=F(Y)\} = \bigcap \{Y\mid(Y)\subseteq Y\}$
\item $\bb{lfp}(F)=X^\infty$
\bi
\item $F(X^\infty)=X^\infty$
\item $X^0 \subseteq Y$ for all $Y\in W$. By induction, if $X^i\subseteq Y$, by monotonicity, $F(X^i) \subseteq F(Y) \subseteq Y$. Hence, $X^{i+1}\subseteq Y$.
\ei
\ei

Suppose $F$ is inflationary: that is $Y\subseteq F(Y)$ for all $Y$. Then $F$ is inductive; the sequence \eqref{eqn:seq} is increasing and reaches a fixed point $X^\infty$.

Suppose $G$ is an arbitrary operator. We associate an inflationary operator $G_{infl}$ defined by $G_{infl}(Y)=Y\cup G(Y)$. Then $X^\infty$ for $G_{infl}$ is called the \ii{inflationary fixed point} of $G$, denoted by $\bb{ifp}(G)$.
$$\bb{ifp}(G)=\bigcup_i X^i, \hbox{ where } X^0=\emptyset, X^{i+1}=X^i\cup G(X^i)$$

Consider an arbitrary operator $F: p(U) \rightarrow p(U)$ and the sequence \eqref{eqn:seq}. This sequence does not need to be inductive. The \ii{partial fixed point} of $F$ is 
\beeq 
\bb{pfp}(F)= \left\{
\ba {lcl}
X^n & \hbox{ if } & X^n=X^{n+1}\\
\emptyset &\hbox{ if } & X^n \neq X^{n+1} \hbox{ for all } n\leq 2^{|U|} 
\ea \right.
\eeeq

Proposition: If $F$ is monotone, then $\bb{lfp}(F)=\bb{ifp}(F)=\bb{pfp}(F).$


\subsection{Fixed Point Logics}

Suppose we have a relational vocabularu $\sigma$, and an additional relation symbol $R \notin \sigma$ of arity k.
Let $\varphi(R,x_1,\dots,x_k)$ be a formula of vocabulary $\sigma \cup \{R\}$. For each $\mathfrak{A} \in \textup{STRUCT}[\sigma]$, the formula $\varphi(R,\vec{x})$ gives rise to an operator $F_\varphi : p(A^k)\rightarrow p(A^k)$ defined as:
$$F_\varphi(X)=\{\vec{a} \mid \mathfrak{A} \models \varphi(X/R,\vec{a})\}$$
$\varphi(X/R,\vec{a})$ means that $R$ is interpreted as $X$ in $\varphi$
\\

Definitions: IFP and PFP...
\\

Lemma: Testing if $F_\varphi$ is monotone is undecidable for FO formulae $\varphi$.
\\

Given a formula $\varphi$, an occurrence of a relation symbol $R$ in $\varphi$ is \ii{negative} if it is under the scope of an odd number of negations, and is \ii{positive} if it is under the scope of an even number of negations.
$$\exists x \neg R(x) \vee \neg \forall y \forall z \neg (R(y) \wedge \neg R(z))$$

A formula is \ii{positive in $R$} if there are no negative occurences of $R$ in it.
\\

Definition: LFP for a positive formula
\\

Lemma: If $\varphi(R,\vec{x})$ is positive in $R$, then $F_\varphi$ is monotone.
\\

Example: Transitive Closure and Acyclicity

Let $E$ be a binary relation, and let $\varphi(R,x,y)$ be
$$E(x,y) \vee \exists z (E(x,z) \wedge R(z,y))$$
This is positive in $R$. Let $\psi (u,v) = [\bb{lfp}_{R,x,y}\varphi(R,x,y)](u,v)$. What does this formula define?

Consider the operator $F_\varphi$. For a set $X$, we have $F_\varphi(X)=E\cup (E \circ X)$.

Hence, $\psi (u,v)$ defines the transitive closure of $E$. The graph connectivity is LFP-definable by the sentence $\forall u \forall v ~ \psi(u,v).$
\\

Consider graphs whose edge relation is $E$, and the formula $\alpha (S,x)$ given by
$$\forall y (E(y,x) \rightarrow S(y)) $$
This is positive in $S$. The operator $F_\alpha$  takes a set $X$ and returns the set of all nodes $a$ such that all the nodes $b$ from which there is an edge to $a$ are in $X$.
Iterating the operator:
\bi
\item $F_\alpha(\emptyset)$ is the set of nodes of in-degree 0.
\item $F_\alpha(F_\alpha(\emptyset))$ is the set of nodes $a$ such that all nodes $b$ with edges $(b,a)\in E$ have in-degree 0.
\bi
\item $F_\alpha(F_\alpha(\emptyset))$ is the set of nodes $a$ such that all paths ending in $a$ have length at most 1.
\ei
$\cdots$
\item At the $i$th stage of the iteration we get the set of nodes $a$ such that all the paths ending in $a$ have length at most $i$.
\ei
When we reach the fixed point, we have nodes such that all the paths ending in them are finite. Hence, the formula
$$\forall u [\bb{lfp}_{S,x}\alpha(S,x)](u)$$
tests if a graph is acyclic.

\subsection{Properties of \LFP\ and \IFP}

We shall derive two important conclusions:
\bi
\item LFP=IFP on finite structures.
\item a normal form for LFP, showing that nested occurrences of fixed point operators can be eliminated.
\ei

Let $\sigma$ be a relational vocabulary, and $R_1, \dots, R_n$ additional relation symbols, with $R_i$ being of arity $k_i$. Let $\vec{x}_i$ be a tuple of variables of length $k_i$. Consider a sequence $\Phi$ of formulae
\beq \ba c
\varphi_1(R_1,\dots,R_n,\vec{x}_1),\\
\cdots,\\
\varphi_n(R_1,\dots,R_n,\vec{x}_n),\\
\ea \eeq {eqn:family}
of vocabulary $\sigma \cup \{R_1,\dots,R_n\}$. Assume that all $\varphi_i$'s are positive in all $R_j$'s.
Then, for a $\sigma$-structure $\mathfrak{A}$, each $\varphi_i$ defines an operator
$$F_i : p(A^k_1) \times \dots \times p(A^k_n) \rightarrow p(A^k_i)$$
given by
$$F_i(X_1,\dots,X_n) = \{\vec{a}\in A^k_i \mid \mathfrak{A} \models \varphi_i(X/R_1,\dots,X_n/R_n,\vec{a})\}$$
\\

We can combine these operators $F_i$'s into one operator
$$\vec{F}:p(A^k_1)\times\dots\times p(A^k_n)\rightarrow p(A^k_1)\times\dots\times p(A^k_n)$$
given by
$$\vec{F}(X_1,\dots,X_n) = (F_1(X_1,\dots,X_n),\dots,F_n(X_1,\dots,X_n))$$

A sequence of sets $(X_1,\dots,X_n)$ is a \ii{fixed point} of $\vec{F}$ if $\vec{F}(X_1,\dots,X_n)=(X_1,\dots,X_n)$. If for every fixed point $(Y_1,\dots,Y_n)$ we have $X_1 \subseteq Y_1,\dots,X_n\subseteq Y_n$, then it is the least fixed point of $\vec{F}$.
\\

The product $p(A^k_1)\times \dots \times p(A^k_n)$ is partially ordered component-wise by $\subseteq$, and the operator $\vec{F}$ is component-wise monotone.

\beq \ba l
\vec{X}^0=(\emptyset,\dots,\emptyset)\\
\vec{X}^{i+1}=\vec{F}(\vec{X}^i)\\
\vec{X}^\infty = \bigcup_{i=1}^\infty \vec{X}^i = ( \bigcup_{i=1}^\infty \vec{X}_1^i, \dots,  \bigcup_{i=1}^\infty \vec{X}_n^i)
\ea \eeq {eqn:seqmulti}

$\vec{X}^\infty=\bb{lfp}(\vec{F})$
\\

Definition: $\hbox{LFP}^{\hbox{simult}}$..
\\

Theorem: $\hbox{LFP}^{\hbox{simult}}=$LFP.


\subsection{\LFP, \PFP\, and Polynomial Time and Space}

\subsection{\DATALOG\ and LFP}

\begin{itemize}
  \item conjunctive queries: $\land, \exists$
  \item rules; intentional head atoms
  \item recursive
  \item \DATALOG\ program: set of rules + output atom
  \item immediate consequence operator
\end{itemize}

\subsection{Transitive Closure Logic}

\subsection{A Logic for \Ptime?}





%
%  BIBLIOGRAPHY
%

\bibliographystyle{plain}
\bibliography{references}

\end{document}

%%% Local Variables:
%%% fill-column: 72
%%% TeX-PDF-mode: t
%%% TeX-debug-bad-boxes: t
%%% TeX-master: t
%%% TeX-parse-self: t
%%% TeX-auto-save: t
%%% reftex-plug-into-AUCTeX: t
%%% End:
